(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
@(Cons(x, xs), ys) →+ Cons(x, @(xs, ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [xs / Cons(x, xs)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)